es:event_system{i:l}, i:Id, ds:fpf(Id; x.Type{i}). @i discrete ds  prop{i':l} 

latex

Definitions	event_system{i:l}, t  T, Id, Type, x. t(x), x:A. B(x), fpf(A; a.B(a)), x.A(x), top, x:AB(x), id-deq, fpf-dom(eq; x; f), b, {x:A| B(x)} , es-dtype(es; i; x; T), prop{i:l}, x,y. t(x;y), fpf-all(A; eq; f; x,v.P(x;v)), @i discrete ds
Lemmas	fpf-all wf, es-dtype wf, assert wf, fpf-dom wf, id-deq wf, fpf-trivial-subtype-top, fpf wf, Id wf, event system wf